$\forall$${\it ds}$:(Id$\rightarrow$Type), ${\it da}$:(Id$\rightarrow$Knd$\rightarrow$Type), $A$:Type, $X$:Interface(${\it ds}$;${\it da}$;$A$), ${\it es}$:ES, $e$:E.
\\[0ex]es{-}decl(${\it es}$;${\it ds}$;${\it da}$) $\Rightarrow$ ($\uparrow$in{-}interface(${\it es}$;$X$;$e$)) $\Rightarrow$ (interface{-}val(${\it es}$;$X$;$e$) $\in$ ($A$ + Top))